“陳總，您剛才提到的，是算法功能層面的建模和實現。

但我認為，離散數學在智能駕駛領域，還有一個極其關鍵、甚至可以說是命攸關的應用點。”

他頓了頓，目掃過顧南舟，最後定格在陳默臉上，“形式化驗證（Formal Verification）。”

“尤其是對行為決策系統。”

蔣雨宏的語氣帶着金屬般的質。

“我們如何確保設計的決策邏輯，在無限複雜的現實場景中，不會出現致命？

如何證明我們的系統，在理論上就滿足某些最核心的安全屬？

比如，‘永遠不發生撞’（Collision-Free），‘永遠遵守通規則’（Rule pliance）？”

他說話的時候配合上手勢和作，像極了一個指揮家：

“這就需要用時序邏輯（Temporal Logic），比如線時序邏輯（LTL - Liemporal Logic）或計算樹邏輯（CTL - putation Tree Logic），來確地形式化描述這些安全屬。

然後，利用模型檢測（Model Cheg）等自化的形式化方法，窮盡系統所有可能的狀態和路徑，來嚴格證明或證偽這些屬是否立。”

蔣雨宏的目變得極其嚴肅：

。的蓋覆全完能就程里測路的量海靠是不！命人到係關這“

。鎖枷全安的固堅最上套統系給就，面層輯邏在，上學數在要需們我

。石基的鎖全安把這造打是正，）yroehT atamotuA（論理機自和）cigoL（學輯邏的中學數散離

”。家專的新創法算於亞不為認我，值價其，家專的’書背‘全安統系駛駕自為言語學數用能，法方化式形通個一

”？獵涉有可，域領法方化式形在你，士博顧“：味意的視審一和許期的烈強着帶中神眼，舟南顧向看他

。來下靜安間瞬室公辦

。舟南顧向看地重凝也，斂收稍稍興的上臉鱗金卞

。題難級超的界業前當是也，一之障保極終的地落全安駛駕能智保確是這，證驗化式形

！戰挑和興的烈強更是的來而之隨但，力的大巨一到舟南顧

：答回地晰清而誠坦，目的鱗金卞和宏雨蔣着迎，氣口一吸深他

。一之向方究研的要重間期士博我是正法方化式形，總卞，總蔣“

。證驗自行進技）gehC ledoM cilobmyS（測檢型模號符用利並，屬活與全安的）序程程線多如（統系發併畫刻）LTC/LTL（輯邏序時用長擅其尤，）gehC ledoM（測檢型模攻主我

”。率效證驗了升提著顯，架框證驗化式形的自半個一了現實並計設，議協式佈分的定特類一對針是就，分部心核文論士博的我

：信自和謹嚴的學着帶氣語，頓了頓他

。的通相是）等釋解象、算計點不、示表態狀化號符（礎基論理的心核但，多得雜複大龐統系的究研前之我比會間空態狀的統系策決駛駕自然雖“

”！向方的力潛大巨有且行可是，障保全安的統系策決於用應度深法方化式形將，新創法算和化優對針行進識知域領駛駕能智合結，信相我

。彩的興出放綻次再上臉，聲一喝低住不忍鱗金卞”！好“

！個這是就的要“

！頭骨啃敢，實紮礎基論理

！了援強的樣這你要需太可組證驗策決們我，士博顧